$\forall$$R$:Realizer. ($\neg$($\uparrow$Rplus?($R$))) $\Rightarrow$ ($\neg$($\uparrow$Rnone?($R$))) $\Rightarrow$ ([[$R$]] $\sim$ @R{-}loc($R$): R{-}base{-}ma($R$))